Write a small C function in file test.c:
int main(int i) { int x = i; if(i > 8) x = 8; return x; }If GCC is not installed, use test.i instead of test.c (.i corresponds to already-preprocessed files).
Launch the analysis and obtain a textual report of the analysis:
$ frama_c_codex -codex test.c -codex-exp-dump -main main
[kernel] Parsing test.c (with preprocessing)
[Codex_config] Setting pointer size to 64
$ cat main.cdump
test.c:1.26-27: `i' -> [--..--]
test.c:1.32-37: `i > 8' -> {0; 1}
test.c:1.32-33: `i' -> [--..--]
test.c:1.53-54: `x' -> [-0x80000000..8]
Unproved regular alarms:
Unproved additional alarms:
Proved 0/0 regular alarms
Unproved 0 regular alarms and 0 additional alarms.
Solved 0/0 user assertions, proved 0If you are using Emacs' compilation-mode (probably works also in other editors), you can click on each expression, and they will bring you to the location in the file.
Obtain an HTML report of the analysis:
$ frama_c_codex -codex test.c -main main -codex-html-dump
...That's all to get started! As there are no reported alarms, your code is memory-safe, free from division-by-zero errors, and free from others errors that Codex checks. The most useful options are:
-codex launches Codex;-main selects the entry point of the analysis;-codex-exp-dump produces a textual dump of all expressions funcname.cdump;-codex-html-dump produces an HTML equivalent of the dump file;-codex-type-file file.typedc uses TypedC specification, useful when analyzing functions independently, which is covered by the types tutorialHappy verification!